判定问题 (Entscheidungsproblem)

概述

Hilbert 于1928年提出的数学基础核心问题：是否存在一种纯机械的算法，能在有限步骤内判定一阶谓词逻辑中任意命题的真假？1936年被 Church 和 Turing 独立证明为不可能，标志着数学推理无法被完全机械化。

是否存在一种算法（definite method），它以一阶谓词逻辑的一个命题作为输入，能够在有限步骤内给出"该命题是普遍有效的（universally valid）"还是"不是"的回答？

关键词是"算法"——一种纯机械的、不需要任何灵感或创造力的、能在有限时间内终止的操作程序。但在1936年之前，"算法"这个概念本身就没有严格的数学定义。

判定问题触及一个根本性的哲学追问：数学推理能否被完全机械化？

Hilbert 试图将全部数学形式化为公理系统，并证明三个关键性质： 1. 一致性：系统内部不会推导出矛盾 2. 完备性：系统中的每一个真命题都能被证明 3. 可判定性：存在机械化方法判定任意命题真假

Godel 不完备定理（1931）已经粉碎了完备性和一致性的期望，但判定问题——作为关于"算法存在性"的问题——仍然悬而未决。

Church 使用 λ 演算证明了判定问题的答案是否定的： - 定义"有效可计算性"为"λ可定义性" - 证明存在不可 λ 定义的函数 - 但 λ 演算高度抽象，缺乏"计算"的直观含义

Turing 用截然不同的方法得出了同样的结论： - 首先精确定义了"算法"（通过图灵机模型） - 证明了停机问题不可判定 - 由此推导出判定问题不可解：如果判定问题可解，则停机问题也可判定——矛盾

Turing 的方法具有 Church 的方法所不具备的优势：图灵机可以被想象为一台物理机器，任何人都能理解其工作方式。

Turing 的论证路线：如果判定问题可解 → 存在算法判定一阶逻辑中任意命题的真假 → 特别地，能判定"存在一台图灵机 M，在输入 w 上执行 n 步后停机" → 通过搜索所有可能的 n，这将能判定 M 在 w 上是否最终停机 → 但停机问题不可判定 → 因此判定问题也不可判定。

与 Godel 不完备定理一起，判定问题的否定回答彻底终结了 Hilbert 纲领： - Godel（1931）：数学有不可证的真命题（完备性的边界） - Turing/Church（1936）：有不可判定的问题（算法能力的边界）

合并解读：数学真理的范围永远超出任何形式系统，算法的能力也有根本限制——数学推理不能被完全机械化。